0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 85 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 69 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 PiDPToQDPProof (⇒, 0 ms)
↳16 QDP
↳17 QDPOrderProof (⇔, 41 ms)
↳18 QDP
↳19 QDPOrderProof (⇔, 0 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 TRUE
PERM1A_IN_GA(.(X1, X2), .(X1, X3)) → U2_GA(X1, X2, X3, perm1A_in_ga(X2, X3))
PERM1A_IN_GA(.(X1, X2), .(X1, X3)) → PERM1A_IN_GA(X2, X3)
PERM1A_IN_GA(.(X1, X2), .(X3, X4)) → U3_GA(X1, X2, X3, X4, selectB_in_aga(X3, X2, X5))
PERM1A_IN_GA(.(X1, X2), .(X3, X4)) → SELECTB_IN_AGA(X3, X2, X5)
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U1_AGA(X1, X2, X3, X4, selectB_in_aga(X1, X3, X4))
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → SELECTB_IN_AGA(X1, X3, X4)
PERM1A_IN_GA(.(X1, X2), .(X3, X4)) → U4_GA(X1, X2, X3, X4, selectcB_in_aga(X3, X2, X5))
U4_GA(X1, X2, X3, X4, selectcB_out_aga(X3, X2, X5)) → U5_GA(X1, X2, X3, X4, perm1A_in_ga(.(X1, X5), X4))
U4_GA(X1, X2, X3, X4, selectcB_out_aga(X3, X2, X5)) → PERM1A_IN_GA(.(X1, X5), X4)
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U10_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
U10_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
PERM1A_IN_GA(.(X1, X2), .(X1, X3)) → U2_GA(X1, X2, X3, perm1A_in_ga(X2, X3))
PERM1A_IN_GA(.(X1, X2), .(X1, X3)) → PERM1A_IN_GA(X2, X3)
PERM1A_IN_GA(.(X1, X2), .(X3, X4)) → U3_GA(X1, X2, X3, X4, selectB_in_aga(X3, X2, X5))
PERM1A_IN_GA(.(X1, X2), .(X3, X4)) → SELECTB_IN_AGA(X3, X2, X5)
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → U1_AGA(X1, X2, X3, X4, selectB_in_aga(X1, X3, X4))
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → SELECTB_IN_AGA(X1, X3, X4)
PERM1A_IN_GA(.(X1, X2), .(X3, X4)) → U4_GA(X1, X2, X3, X4, selectcB_in_aga(X3, X2, X5))
U4_GA(X1, X2, X3, X4, selectcB_out_aga(X3, X2, X5)) → U5_GA(X1, X2, X3, X4, perm1A_in_ga(.(X1, X5), X4))
U4_GA(X1, X2, X3, X4, selectcB_out_aga(X3, X2, X5)) → PERM1A_IN_GA(.(X1, X5), X4)
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U10_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
U10_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → SELECTB_IN_AGA(X1, X3, X4)
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U10_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
U10_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
SELECTB_IN_AGA(X1, .(X2, X3), .(X2, X4)) → SELECTB_IN_AGA(X1, X3, X4)
SELECTB_IN_AGA(.(X2, X3)) → SELECTB_IN_AGA(X3)
From the DPs we obtained the following set of size-change graphs:
PERM1A_IN_GA(.(X1, X2), .(X3, X4)) → U4_GA(X1, X2, X3, X4, selectcB_in_aga(X3, X2, X5))
U4_GA(X1, X2, X3, X4, selectcB_out_aga(X3, X2, X5)) → PERM1A_IN_GA(.(X1, X5), X4)
PERM1A_IN_GA(.(X1, X2), .(X1, X3)) → PERM1A_IN_GA(X2, X3)
selectcB_in_aga(X1, .(X1, X2), X2) → selectcB_out_aga(X1, .(X1, X2), X2)
selectcB_in_aga(X1, .(X2, X3), .(X2, X4)) → U10_aga(X1, X2, X3, X4, selectcB_in_aga(X1, X3, X4))
U10_aga(X1, X2, X3, X4, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
PERM1A_IN_GA(.(X1, X2)) → U4_GA(X1, X2, selectcB_in_aga(X2))
U4_GA(X1, X2, selectcB_out_aga(X3, X2, X5)) → PERM1A_IN_GA(.(X1, X5))
PERM1A_IN_GA(.(X1, X2)) → PERM1A_IN_GA(X2)
selectcB_in_aga(.(X1, X2)) → selectcB_out_aga(X1, .(X1, X2), X2)
selectcB_in_aga(.(X2, X3)) → U10_aga(X2, X3, selectcB_in_aga(X3))
U10_aga(X2, X3, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
selectcB_in_aga(x0)
U10_aga(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PERM1A_IN_GA(.(X1, X2)) → PERM1A_IN_GA(X2)
POL(.(x1, x2)) = 1 + x2
POL(PERM1A_IN_GA(x1)) = 1 + x1
POL(U10_aga(x1, x2, x3)) = 1 + x3
POL(U4_GA(x1, x2, x3)) = 1 + x3
POL(selectcB_in_aga(x1)) = 1 + x1
POL(selectcB_out_aga(x1, x2, x3)) = 1 + x3
selectcB_in_aga(.(X1, X2)) → selectcB_out_aga(X1, .(X1, X2), X2)
selectcB_in_aga(.(X2, X3)) → U10_aga(X2, X3, selectcB_in_aga(X3))
U10_aga(X2, X3, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
PERM1A_IN_GA(.(X1, X2)) → U4_GA(X1, X2, selectcB_in_aga(X2))
U4_GA(X1, X2, selectcB_out_aga(X3, X2, X5)) → PERM1A_IN_GA(.(X1, X5))
selectcB_in_aga(.(X1, X2)) → selectcB_out_aga(X1, .(X1, X2), X2)
selectcB_in_aga(.(X2, X3)) → U10_aga(X2, X3, selectcB_in_aga(X3))
U10_aga(X2, X3, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
selectcB_in_aga(x0)
U10_aga(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PERM1A_IN_GA(.(X1, X2)) → U4_GA(X1, X2, selectcB_in_aga(X2))
POL(.(x1, x2)) = 1 + x2
POL(PERM1A_IN_GA(x1)) = x1
POL(U10_aga(x1, x2, x3)) = 1 + x3
POL(U4_GA(x1, x2, x3)) = x3
POL(selectcB_in_aga(x1)) = x1
POL(selectcB_out_aga(x1, x2, x3)) = 1 + x3
selectcB_in_aga(.(X1, X2)) → selectcB_out_aga(X1, .(X1, X2), X2)
selectcB_in_aga(.(X2, X3)) → U10_aga(X2, X3, selectcB_in_aga(X3))
U10_aga(X2, X3, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
U4_GA(X1, X2, selectcB_out_aga(X3, X2, X5)) → PERM1A_IN_GA(.(X1, X5))
selectcB_in_aga(.(X1, X2)) → selectcB_out_aga(X1, .(X1, X2), X2)
selectcB_in_aga(.(X2, X3)) → U10_aga(X2, X3, selectcB_in_aga(X3))
U10_aga(X2, X3, selectcB_out_aga(X1, X3, X4)) → selectcB_out_aga(X1, .(X2, X3), .(X2, X4))
selectcB_in_aga(x0)
U10_aga(x0, x1, x2)